Lean Game Server

Lean Game Server

Natural Number Game

https://scrapbox.io/files/68e5470c490f753855e68b40.png

初歩的な操作から初めて、

足し算、

掛け算、

論理包含(条件文)..

べき乗

...

の定理を証明していく

ペアノの公理という題材も良い

証明は簡単だから

公理から導かれることの組み合わせで、我々の手のなじみのある数学的構造を作ることが主題

ゼロから構築してる感がわかる

初手から高等数学以上の証明を書くのは多分大変なんじゃないの？知らんけど

さっさと書き始めて覚えるほうが正しい

初手でドキュメントをちまちま読んでも仕方がない

Leanでの証明は、

条件とゴールを定めて、

条件に対しての加工をコードに書いて

ゴールを満たすようにして定理を示す

この過程は、加工の記述はコードであるが、加工途中の可変な状態である条件とゴールは、見えない

エディタ上でリアルタイムに右側のinfoviewで見る必要がある

よって、REPL環境で使うことが大前提

Lean Game Serverを触ったうえでのLeanの理解

数学の証明を、コードでかける

仮定が引数。証明すべき命題は返り値の型

さまざまな証明過程の操作をtacticとして、関数内に記述していく

tacticを使って、仮定やゴールを加工する

ゴールが成立したら証明完了

ここの理論的背景が気になるところではあるものの

プログラミングをするのに型システムやTaPLが不要なのと同様に

数学の証明をLeanで書くためには、Leanのこの「証明」という手続きをどうやって型システムで表現するか、ということの背景は気にせんで良い

もちろん、気になって勉強するのも一興

命題は型で、証明はその項